ESAxioms{i:l}(E;T;M;loc;kind;val;when;after;time;sends;sender;index;first;pred;causl)
== (e, e':E. (loc(e) = loc(e'))  ((causl(e,e'))  (e = e')  (causl(e',e))))
== & (e:E. ((first(e)))  (e':E. (loc(e') = loc(e))  ((causl(e',e)))))
== & (e:E.
== & ((((first(e))))
== & ( (loc(pred(e)) = loc(e) & causl(pred(e),e)
== & ( & (e':E. (loc(e') = loc(e))  ((causl(pred(e),e') & causl(e',e))))))
== & (e:E.
== & ((((first(e))))
== & ( (x:Id, t:. when(x,e,t) = after(x,pred(e),t + ((time(e)) - (time(pred(e)))))))
== & Trans(E;e,e'.causl(e,e'))
== & SWellFounded(causl(e,e'))
== & (e:E.
== & ((isrcv(kind(e)))
== & ( ((sends(lnk(kind(e)),sender(e)))[(index(e))] = msg(lnk(kind(e));tag(kind(e));val(e))))
== & (e:E. (isrcv(kind(e)))  (causl(sender(e),e)))
== & (e, e':E.
== & ((causl(e,e'))
== & ( (((((first(e')))) c ((causl(e,pred(e')))  (e = pred(e'))))
== & (  ((isrcv(kind(e'))) c ((causl(e,sender(e')))  (e = sender(e'))))))
== & (e:E. (isrcv(kind(e)))  (loc(e) = destination(lnk(kind(e)))))
== & (e:E, l:IdLnk. ((loc(e) = source(l)))  (sends(l,e) = []))
== & (e, e':E.
== & ((isrcv(kind(e)))
== & ( (isrcv(kind(e')))
== & ( (lnk(kind(e)) = lnk(kind(e')))
== & ( ((causl(e,e'))
== & (  ((causl(sender(e),sender(e')))
== & (   (sender(e) = sender(e') & ((index(e)) < (index(e')))))))
== & (e:E, l:IdLnk, n:{0..||sends(l,e)||}.
== & (e':E. ((isrcv(kind(e'))) c (lnk(kind(e')) = l & sender(e') = e & index(e') = n))) 

latex

---

clarification:

ESAxioms{i:l}
ESAxioms(E; T; M; loc; kind; val; when; after; time; sends; sender; index; first; pred; causl)
== (e:E, e':E. (loc(e) = loc(e')  Id)  ((causl(e,e'))  (e = e'  E)  (causl(e',e))))
== & (e:E. ((first(e)))  (e':E. (loc(e') = loc(e)  Id)  ((causl(e',e)))))
== & (e:E.
== & ((((first(e))))
== & ( (loc(pred(e)) = loc(e)  Id & causl(pred(e),e)
== & ( & (e':E. (loc(e') = loc(e)  Id)  ((causl(pred(e),e') & causl(e',e))))))
== & (e:E.
== & ((((first(e))))
== & ( (x:Id, t:.
== & ( when(x,e,t) = after(x,pred(e),t + ((time(e)) - (time(pred(e)))))  T(loc(e),x)))
== & Trans(E;e,e'.causl(e,e'))
== & strongwellfounded(E; e,e'.(causl(e,e')))
== & (e:E.
== & ((isrcv(kind(e)))
== & ( ((sends(lnk(kind(e)),sender(e)))[(index(e))]
== & ( (=
== & ( (msg(lnk(kind(e));tag(kind(e));val(e))
== & ( ( Msg(M)))
== & (e:E. (isrcv(kind(e)))  (causl(sender(e),e)))
== & (e:E, e':E.
== & ((causl(e,e'))
== & ( (((((first(e')))) c ((causl(e,pred(e')))  (e = pred(e')  E)))
== & (  ((isrcv(kind(e'))) c ((causl(e,sender(e')))  (e = sender(e')  E)))))
== & (e:E. (isrcv(kind(e)))  (loc(e) = destination(lnk(kind(e)))  Id))
== & (e:E, l:IdLnk. ((loc(e) = source(l)  Id))  (sends(l,e) = []  (Msg_sub(l;M) List)))
== & (e:E, e':E.
== & ((isrcv(kind(e)))
== & ( (isrcv(kind(e')))
== & ( (lnk(kind(e)) = lnk(kind(e'))  IdLnk)
== & ( ((causl(e,e'))
== & (  ((causl(sender(e),sender(e')))
== & (   (sender(e) = sender(e')  E & ((index(e)) < (index(e')))))))
== & (e:E, l:IdLnk, n:{0..||sends(l,e)||}.
== & (e':E
== & (((isrcv(kind(e')))
== & (c (lnk(kind(e')) = l  IdLnk & sender(e') = e  E & index(e') = n  ))) 

latex

Definitions	, r + s, r - s, Trans(T;x,y.E(x;y)), SWellFounded(R(x;y)), Msg(M), l[i], msg(l;t;v), tag(k), destination(l), A, Id, source(l), type List, Msg_sub(l;M), [], P  Q, P  Q, P  Q, a < b, x:A. B(x), {i..j}, #$n, ||as||, x:A. B(x), A c B, b, isrcv(k), IdLnk, lnk(k), P & Q, s = t, , f(a)
FDL editor aliases	ESAxioms